/* constraint 
         (\forall f. (f \in Desugared <--> (
             f \in Tru |
             (f \in IOr & IOr_getField_l(f) \in Desugared & IOr_getField_r(f) \in Desugared))))
*/
  
/* domain
        Dom_IOr = IOr 
*/
sealed abstract class TopF
class Tru extends TopF
class Flse extends TopF
class IOr(val l: TopF, val r: TopF) extends TopF 


object IOr {
   def apply(l: TopF, r: TopF): IOr = 
        /* postcondition (l \in Desugared & r \in Desugared) --> res \in Desugared
        */
     new IOr(l,r)
   def unapply(ior: IOr): Option[(TopF,TopF)] =
        /* postcondition ior \in Desugared --> (res1 \in Desugared & res2 \in Desugared) */
     Some(Tuple2(ior.l,ior.r))
}

object Main {
  
  def desugar(f: TopF): TopF = 
    /* postcondition res \in Desugared */
    (f: TopF) match {
      case t: Tru => t
      case t: Flse => new Tru()
      case IOr(l: TopF, r: TopF) => IOr(this.desugar(l),this.desugar(r))
    }

  def mirror(f : TopF) : TopF = 
   /* precondition f \in Desugared
      postcondition res \in Desugared */
  (f : TopF) match {
     case t: Tru => t
     case IOr(l:TopF,r:TopF) => IOr(this.mirror(r),this.mirror(l))
  }

  def test(t: TopF): Boolean = (this.desugar(t): TopF) match {
    case t: Tru => true
    case IOr(l:TopF,r:TopF) => this.test(l) && this.test(r)
  }
}
